;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;CS 710 - AI - Program 2 - Fall 2012
;Author: Justin J. Ploegert (ploegert@uwm.edu)
;mp3_demo.lisp
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(load "p3-fun.lisp")
(load "p3-testfun.lisp")



(defun run-parte-tests ()
  
  
;====================================================================
; PART a - WFP Value
  (write-line (format nil "============================"))
  (write-line (format nil "Running tests for part a...- WFP-CHECKER"))
  (write-line (format nil "============================"))
  (part_a '((P124) ("John is up") (NOT (P)) (AND (P)(Q)) (OR (P)(Q)) (IMPLIES (P)(Q)) (EQUIV (P)(Q)) (EQUIV (IMPLIES (P) (AND (P)(Q))) (NOT (OR (P) (IMPLIES (P)(Q))))) (|p|) (8up) (|not| (P)) (AND (|p|)(Q)) ((P) OR (Q))))
  
;====================================================================
; PART B1 - Truth Value
  (write-line (format nil "============================"))
  (write-line (format nil "Running tests for part b1...- TruthValue"))
  (write-line (format nil "============================"))
  
  (setf sentence '((AND (P)(Q)) (OR (P)(Q)) (IMPLIES (P)(Q)) (EQUIV (P)(Q)) 
(EQUIV (IMPLIES (P1) (AND (P2) (Q3))) (NOT (OR (P4) (IMPLIES (P5)(Q6)))))
(IMPLIES (P)(P)) (EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q))) (EQUIV (NOT   
(AND (P)(Q))) (OR (NOT (P))(NOT (Q)))) (IMPLIES (P) (IMPLIES (Q)(P))) (OR
(P) (NOT (P)))))
  (setf interpretation '((P nil) (Q nil) (P1 t) (P2 nil) (Q3 t) (P4 nil) (P5 t) (Q6 nil)))
  (write-line (format nil "Sentence is: ~a" sentence))
  (write-line (format nil "Interpretation is: ~a" interpretation))
  (part_b sentence interpretation)
  
;====================================================================
; PART B2 -- IsTautology
  (write-line (format nil "============================"))
  (write-line (format nil "Running tests for part b2...-IsTautology"))
  (write-line (format nil "============================"))
  (setf sentence '((NOT (P)) (AND (P)(Q)) (OR (P)(Q)) (IMPLIES (P)(Q)) (EQUIV (P)(Q)) 
(EQUIV (IMPLIES (P1) (AND (P2) (Q3))) (NOT (OR (P4) (IMPLIES (P5)(Q6)))))
(IMPLIES (P)(P)) (EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q))) (EQUIV (NOT   
(AND (P)(Q))) (OR (NOT (P))(NOT (Q)))) (IMPLIES (P) (IMPLIES (Q)(P))) (OR
(P) (NOT (P)))))
  (part_b_tautology sentence)
  
;====================================================================================================
; PART C -- wfp-checkerFOL
  (write-line (format nil "============================"))
  (write-line (format nil "Running tests for part c...WFP-CHECKERFOL"))
  (write-line (format nil "============================"))

  (part_c '((NOT (P |x| |y| |z|)) (P (|f| |b| |y|) |y|) 
          (IMPLIES (Q |u| (|f| |a| |v|) |d|) (R (|g| (|h| |b| |c| |w|)) |y|)) 
          (ALL |x| (IMPLIES (A |x| |c|) (B |x| |d|))) 
          (ALL |x| (EXISTS |y| (IMPLIES (A |y|) (B |x|)))) 
          (AND (ALL |x| (P |x|)) (Q |y| |z|)) 
          (EQUIV (B |f| |u| |a|) (P ())) (P |x| |a| Q)
          (ALL |x| |y| (P |x| |y|)) (ALL |x| (IMPLIES (A |y| |c|) (B |x| |d|))) 
          (ALL |z| (EXISTS |y| (IMPLIES (A |y|) (B |x|))))))
    

;====================================================================================================
; PART D -- wfp-checkerFOL
  (write-line (format nil "============================"))
  (write-line (format nil "Running tests for part D...STRIPES"))
  (write-line (format nil "============================"))
  
  (part_d)
  
  
 
  )


(run-parte-tests)
;(parta-tests)
;(partb-tests)
;(partc-tests)